package kodkod.analysis;

import java.util.ArrayList;

import kodkod.analysis.ordering.AbstractOrdering;
import kodkod.engine.fol2sat.Translation;

public class Experiment {
	
	final int TIMEOUT = 900000;
	final int REPEAT_TIMEOUT = 1000; // conduct experiment only once, if one run lasts longer than that value
	
	final long MEMOUT = 2147483648L;
	
	boolean timeout = false;
	boolean repeat_timeout = false;
	boolean memout = false;
	
	ArrayList<Long> times = new ArrayList<Long>();
	int nofConflicts = 0;
	int translationTime = 0;
	
	Problem problem;
	AbstractOrdering ordering;
	
	public Experiment(Problem problem, AbstractOrdering ordering) {
		this.problem = problem;
		this.ordering = ordering;
	}
	
	public ArrayList<Long> getTimes() {
		return times;
	}
	
	public int getTranslationTime() {
		return translationTime;
	}
	
	public long getTimeAverage() {
		if (times.size() > 0) {
			if (times.get(0) == -1) {
				return -1;
			} else {
				long total = 0;
				for (long time : times) total += time;
				return total / times.size();
			}
		} else {
			return 0;
		}
	}
	
	public long getTimeVariance() {
		long var = 0;
		long avg = getTimeAverage();
		if (avg != -1) {
			for (long time : times) {
				var += (time - avg) * (time - avg);
			}
			return Math.round(Math.sqrt(var / times.size()));
		} else {
			return -1;
		}
	}
	
	public int getNumberOfConflicts() {
		return this.nofConflicts;
	}
	
	public boolean conduct(int n) {		
		for (int run = 0; run < n && !timeout && !repeat_timeout; run++) {
			conduct();
		}		
		System.gc();
		
		return !timeout && !memout;
	}
	
	public void conduct() {
		try {
			long startTranslate = System.currentTimeMillis();
			Translation translation = problem.getTranslation(this.ordering);
			long endTranslate = System.currentTimeMillis();
			this.translationTime = (int)(endTranslate - startTranslate);
	
			SolverThread solver = new SolverThread(translation.cnf());
			
			boolean finished = false;
			solver.setPriority(Thread.MAX_PRIORITY);
			long startSolve = System.currentTimeMillis();
			solver.start();	
			
			while (!timeout && !memout && !finished) {
				finished = solver.time != -1;
				timeout = (System.currentTimeMillis() - startSolve) > TIMEOUT && TIMEOUT > 0;
				memout = Runtime.getRuntime().totalMemory() > MEMOUT || Runtime.getRuntime().freeMemory() < 1024000;
				repeat_timeout = (System.currentTimeMillis() - startSolve) > REPEAT_TIMEOUT && REPEAT_TIMEOUT > 0;
								
				if (timeout || memout) {
					solver.stopSolver();
					
					try {
						solver.join();
					} catch (InterruptedException e) {
						e.printStackTrace();
					}
				} else if (!finished) {
					try {
						Thread.sleep(100);
					} catch (InterruptedException e) {
						e.printStackTrace();
					}
				}
			}
			
			times.add(solver.time);
			this.nofConflicts = solver.getNumberOfConflicts();
			if (!timeout && !memout) problem.satisfiable = solver.isSat;
		} catch (OutOfMemoryError e) {
			memout = true;
		}
	}
	
	public String toString() {
		if (!timeout && !memout) {
			long time = getTimeAverage();
			long variance = getTimeVariance();
			StringBuffer buf = new StringBuffer();
			buf.append("Time:");
			buf.append(time);
			buf.append("ms");
			if (variance > time) {
				buf.append(" Variance:");
				buf.append(variance);	
			}
			buf.append(" Conflicts:" + nofConflicts);
			if (problem.satisfiable) {
				buf.append(" satisfiable");
			} else {
				buf.append(" unsatisfiable");
			}
			return buf.toString();
		} else if (timeout) {
			return "TIMEOUTms Conflicts -1";
		} else {
			return "MEMOUTms Conflicts -1";
		} 
	}

}
